Nuprl Lemma : R-restrict_functionality
11,40
postcript
pdf
A
,
B
:Realizer,
ns
,
ms
:(MaName List).
A
B
ns
ms
A
|
ns
B
|
ms
latex
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
Lemmas
R-restrict
wf
,
R-sub
transitivity
,
es
realizer
wf
,
R-sub
wf
,
MaName
wf
,
l
contains
wf
,
R-restrict
functionality
wrt
l
contains
,
R-restrict
functionality
wrt
R-sub
origin
A, B:Realizer, ns, ms:(MaName List). A 
B 
ns ms A|ns B|ms A, B:Realizer, ns, ms:(MaName List). A B ns ms A|ns B|ms 
T